(set-logic QF_UF)
(set-info :status unsat)
(declare-sort U 0)
(declare-fun b () U)
(declare-fun f (Bool) U)
(assert (= b (f (not (= b (f true))))))
(assert (not (= b (f true))))
(check-sat)
